Proving soundness is essential in the face of complexities
    such as wildcards and raw/cooked objects.
This section gives the typing rules and operational semantics of a simplified version of OIGJ
    and sketches the proofs of our immutability and ownership guarantees.
For lack of space, the full proofs are included in our technical report~\cite{ZibinUpdated2010}.

% done: change Gamma[K] and H[K] into K

Our type system, called Featherweight OIGJ (FOIGJ),
    is based on Featherweight Java (FJ)~\cite{Igarashi:2001:FJM}.
FOIGJ models the essence of OIGJ:
    the fact that every object has an ownership and immutability,
    and the cooking phase when creating immutable objects.
FOIGJ adds imperative constructs to FJ,
    such as \code{null} values, field assignment, locations/objects, and a heap.
FOIGJ also adds a constructor body (to model the cooking phase),
    owner and immutability parameters to classes,
    guards as in cJ~\cite{HuangZS2007:cJ},
    wildcard owners,
    and the run-time notion of raw/cooked objects.


FOIGJ poses two main challenges:
    (i)~modeling \emph{wildcards} in the typing rules,
    and (ii)~the representation for \emph{raw objects}.
We use the following example (similar to \Ref{Figure}{OIGJ-example}) to demonstrate these two challenges:
\begin{algorithmic}
\STATE \code{class Foo<O,I> \lb}
\STATE \code{~Date\hgn{{O},{I}} sameD;}
\STATE \code{~Date\hgn{{\This},I} ownedD;}
\STATE \code{~Date\hgn{{\This},Immut} immutD;}
%\STATE \code{}
\STATE \code{~\underline{<I extends Raw>?} void Foo()\lb}
\STATE \code{~~~this.ownedD = new Date\hgn{This,\underline{I}}();}
\STATE \code{~~~this.immutD = new Date\hgn{This,\underline{Immut}}();}
\STATE \code{~~~\ldots~\rb~\rb}
%\STATE \code{~~~this.ownedD.setTime(\ldots);}
%\STATE \code{~\rb}
%\STATE \code{\rb}
\end{algorithmic}

Wildcards pose a difficulty due to a process in Java called \emph{wildcard capture} in which
    a wildcard is replaced with a fresh type variable.
For example, the two underlined wildcards below might represent two distinct owners:
\begin{algorithmic}
\STATE \code{Foo<\underline{?},I> f = \ldots;}
\STATE \code{Date<\underline{?},I> d = \ldots;}
\STATE \code{f.sameD = d;} \myCOMMENT{Illegal assignment! Different owners! } % for \code{f} and \code{d}.}
\end{algorithmic}
A Java compiler rejects the assignment
    due to incompatible types, because the wildcards were captured by different type variables.
Formalizing the full power of wildcards (with upper and lower bounds)
    was only recently achieved~\cite{CameronDE2008}.
FOIGJ does \emph{not} model wildcard capture.
Instead, it is enough to augment
    the field assignment rule
    with the following check:
    assigning to~$o$ is illegal if~$\Ofn{o}=\code{?}$ (similarly for method invocation).
This extra check is needed only in FOIGJ, and not in OIGJ, because OIGJ is built on top of Java, which supports wildcard capture.
%We stress that \textbf{Field assignment rule} does need this check because it is done by the Java's compiler.

The second challenge is modeling raw objects in the \emph{non-erased} operational semantics.
Recall that generics are erased in Java and are not present at run time.
FOIGJ's \emph{erased} operational semantics is identical to that of normal Java:
    ownership and immutability information is not kept.
In contrast, the \emph{non-erased} version stores with each object its owner and immutability,
    and it checks at run time the ownership and immutability guarantees
    (i.e., that field assignment respects owner-as-dominator and
    is done only on mutable or raw objects).
The non-erased version is used only in the formalism.
    Storing the owner and immutability of every object at run time would be
a huge overhead, and is not required for correctness if the program
satisfies OIGJ's type rules.

The non-erased semantics of Featherweight Generic Java~\cite{Igarashi:2001:FJM} (FGJ)
    performs variable substitution for method calls,
    however FGJ's way of doing substitution does not work in FOIGJ.
For example, consider the following reduction as done in imperative FGJ: % (augmented with assignments)
\begin{algorithmic}
\STATE $\code{new Foo<World,\underline{Immut}>()} \reducesto$
\STATE ~~~~~~~~~~~~~~~~~~~~~~~~~~~$\code{~l.ownedD = new Date\hgn{l,\underline{Immut}}();}$
\STATE ~~~~~~~~~~~~~~~~~~~~~~~~~~~$\code{~l.immutD = new Date\hgn{l,\underline{Immut}}();}\ldots$
\end{algorithmic}
The variable \hI in the constructor was substituted with \Immut,
    and the variables \this and \This were substituted with a new location~\hl
    that was created on the heap,
    i.e., the heap~$H$ now contains a new object  in location~\hl whose fields are all \code{null}:~~
    $H = \{ \hl \mapsto \code{Foo<World,Immut>(}\ol{\code{null}}\code{)} \}$.
(Locations are pointers to objects; we treat locations and objects identically because they have a one-to-one mapping,
    e.g., the owner of a location is defined to be the owner of its object.)
Note how owner parameters ($\Ofn{o}$) at compile time are replaced with owners ($\Owner{o}$) at run time,
    e.g., \This was replaced with location~\hl.

There are two reasons why substituting \hI with \Immut does not work in FOIGJ:
(i)~the reduction does not type-check because we mutate an immutable object (\code{l.ownedD = \ldots}),
and (ii)~we lost information about the two new \code{Date} objects,
    namely that \code{ownedD} can still be mutated after its constructor finishes (because it is \this-owned)
     whereas \code{immutD} cannot.

FOIGJ solves these two issues by introducing an auxiliary type~$\Immut_\hl$.
An object~$o$ of immutability~$\Ifn{o}=\Immut_\hl$
    becomes cooked when the constructor of \hl finishes,
    therefore we call~$\hl$ its \emph{cooker}, denoted by~$\Cooker{o}=\hl$.
Phrased differently, an object is cooked when its cooker is \emph{constructed} (i.e., the cooker's constructor finishes).
Note that the cooker~$\hl$ can be~$o$ itself, its owner, or even some other incomparable object.

The connection between the cooker and the owner will be shown in the subtyping and typing rules below.
Intuitively, for a reference of type~$\code{C<o,Immut}_\hl\code{>}$,
    if the cooker~\hl is not inside the owner~\ho, then that reference must point to an object whose cooker is~\hl.
Otherwise (if~\hl is inside~\ho), then that reference might point to any cooked immutable object (even one with a cooker that is not~\hl).

%A cooked object has the following properties:
%    (i)~it cannot be mutated further,
%    and (ii)~it points only to cooked objects (it can point to raw objects via readonly references).
%(Raw objects can point to any object.)
In our example,
    the location~\hl that was created with \code{new Foo<World,\underline{Immut}>()}
    becomes cooked when it is constructed, i.e.,~$\Cooker{\hl}=\underline{\hl}$, and
    $H = \{ \hl \mapsto \code{Foo<World,Immut}_{\underline{\hl}}\code{>(}\ol{\code{null}}\code{)} \}$.
Now FGJ's way of doing the substitution works for FOIGJ,
    because \hI is replaced with~$\Immut_\hl$,
    i.e.,\\
    $\code{~l.ownedD = new Date<l,}\underline{\Immut_\hl}\code{>();}$\\
    $\code{~l.immutD = new Date\hgn{l,\underline{Immut}}();}$\\
Note how the cooker of \code{ownedD} is~\hl,
    whereas the cooker of \code{immutD} is \code{immutD} itself.
Therefore, \code{ownedD} has a longer cooking phase than \code{immutD}.

FOIGJ also maintains
    the set of currently executing constructors~$K$, where~$K \subseteq \dom{}(H)$.
We maintain the invariant that a location~\hl is \emph{raw} iff~$\Cooker{\hl} \in K$,
    and require that \emph{only mutable or raw objects can be mutated}.
Specifically,~$\Immut_\hl$ is a subtype of \Raw when~$\hl \in K$,
    and it is a subtype of \Immut when~$\hl \not \in K$.

Type~$\Immut_\hl$ also helps understand the \textbf{Object creation rule} better.
Recall that an \Immut object can be created from a \Raw constructor,
    even though \Immut is not a subtype of \Raw,
    which seems to contradict \textbf{cJ's method guard rule}.
However, type~$\Immut_\hl$ is in fact a subtype of \Raw when the object is created,
    because in our typing rules we have that $\Immut_\hl \st \Raw$ iff~$\hl \in K$,
    and when an object is created, its cooker must be in~$K$.
Phrased differently, the type of an immutable object never changes (always $\Immut_\hl$),
    but during the program execution the set $K$ changes, and therefore the subtyping relation changes:
    initially $\Immut_\hl$ is a subtype of \Raw, but later the object becomes cooked,
    and then $\Immut_\hl$ is no longer a subtype of \Raw, but instead it becomes a subtype of~$\Immut$.

\input{formal-syntax}

Faced with such major challenges,
%Similar to the way FJ removed many features from Java (such as null values, assignment, overloading, static, private, etc.),
    we removed from FOIGJ anything that was not needed to prove our run-time guarantees.
Specifically, FOIGJ does \emph{not} model:
    generics (except for the owner and immutability parameters),
    owner polymorphic methods, casting, inner classes, fresh owners,
    or multiple immutability/owner parameters.
On the one hand, the interaction between generics and \emph{immutability} (which enables covariant subtyping)
    was previously proven sound in Featherweight IGJ (FIGJ)~\cite{ZibinPAAKE2007}.
On the other hand, the interaction between generics and \emph{ownership} (as found in the ownership nesting rule)
    was previously proven sound in Featherweight OGJ (FOGJ)~\cite{PotaninNCB2006}.
Because covariant subtyping (as found in IGJ) and ownership nesting (as found in OGJ) was not changed in OIGJ,
    we decided not to model generics in FOIGJ.
We note that FOIGJ does model \Raw, which was not modeled previously in FIGJ.


Consider the typing rules in \Ref{Figure}{oigj-typing-rules}.
Classes in FOIGJ have a single \Raw constructor,
    therefore \textbf{Object creation rule} is always satisfied and can be ignored.
Furthermore, because FOIGJ does not model generics, static, or inner classes,
    then the following rules can also be ignored:
        \textbf{Ownership nesting}, \textbf{Inner classes}, \textbf{Inheritance},
        \textbf{Invariant}, \textbf{Erased signature},
        and
        \textbf{Fresh owners}.
Covariant subtyping and erased signatures were described in FIGJ,
    and ownership nesting and (limited) owner-polymorphic methods in FOGJ.
We stress that FOIGJ \emph{does} model wildcard for the owner parameter (\code{?}), % in \Ref{Figure}{syntax}
    which is used in owner-polymorphic methods such as \code{sort} or \code{equals}.
In our view, extending the formalism with fresh owners or inner classes
    increases the complexity of the calculus without providing new insights.
%    on the interaction between ownership and immutability.

The following rules are enforced by the syntax of FOIGJ (\Ref{Figure}{syntax}):
    \textbf{Generic Wildcards} and
    \textbf{\Raw parameter}.
The remaining rules are:
    \textbf{Field assignment},
    \textbf{Field access},
    \textbf{Method invocation},
    \textbf{cJ's~\cite{HuangZS2007:cJ} method guard},
    and a \textbf{Subtype relation} (without generics).
These rules are formalized in FOIGJ in the subtyping rules of \Ref{Figure}{subtyping} ($\KGdash \hT \st \code{T'}$)
    and the typing rules of \Ref{Figure}{expressions} ($\KGdash \he:\hT$).
Finally, the reduction rules are described in \Ref{Figure}{reduction} ($K \vdash H,\he \reducesto H',\he'$).


\Ref{Section}{syntax} describes the syntax of FOIGJ,
    \Ref{Section}{subtyping} the subtyping rules,
    \Ref{Section}{type-checking} the typing rules,
    \Ref{Section}{reduction} the reduction rules,
    and \Ref{Section}{soundness} proves preservation, progress, and our run-time immutability and ownership guarantees.



\Subsection[syntax]{Syntax of FOIGJ}
FOIGJ adds imperative extensions to FJ such as assignment to fields, object locations, \code{null}, and
    a heap~\cite{pierce:2002:types-and-pls}.
A constructor initializes all the fields to \code{null},
    and then calls a \code{build} method that constructs the object.
Having \code{null} values is important because \this-owned fields must be initialized with \code{null}
    since they cannot be assigned from the outside,
    i.e., they must be created within \this.
For example, a list constructor cannot receive its entries as constructor arguments;
    instead it must create the entries within the \code{build} method.

\Ref{Figure}{syntax} presents the syntax of FOIGJ.
Expressions in FOIGJ include the four expressions in FJ
    (method parameter, field access, method invocation, and new instance creation; \emph{without} casting),
    as well as the imperative extensions (field update,~$\he\code{;return l}$, and values).
Expression~$\code{e;return l}$ is created when reducing a constructor call,
    e.g., $K \vdash \code{new N(\ldots)} \reducesto \code{l.build(\ldots);return l}$,
    then we proceed to reduce~$\code{l.build(\ldots)}$ and finally return \hl.
Note that \hO and \hI are terminals, i.e.,
    the owner and immutability parameters are always named~\hO and \hI.

An evaluation of an expression (\he)
    is either infinite,
    or is stuck on \code{null}-pointer exception,
    or terminates with a value (\hv), which is either \code{null} or a location~\hl.


\input{formal-subtyping}

Note how the syntax limits the usage of wildcards and \Raw:
    wildcards (\code{?}) can be used only as the owner of method arguments (FOIGJ does not have local variables),
    and \Raw only as a method guard (\code{IG}).

We represent sequences using an over-line notation, similarly to FJ, i.e.,
    comma denotes concatenation of sequences,
    and
    $\ol{\code{FT}}~\ol{\hf}\texttt{;}$ represents
    the sequence~$\code{FT}_1~\hf_1\texttt{;}\ldots\code{FT}_n~\hf_n\texttt{;}$

A class in FOIGJ has a single constructor that can create both mutable and immutable objects,
    i.e., it is a \Raw constructor.
The constructor is not shown in the syntax because it can be inferred from the class declaration:
    it always assigns \code{null} to the fields of the newly created object,
    and then invokes this special method (ignoring the return value):\\
\code{<I extends Raw>? \code{T'} build($\ol{\code{T}}~\ol{\he}$) \lb{}~return e; \rb}\\ %
We require that each class has such a method,
    and that its parameters are not \this-owned nor have wildcards.
The reduction rules call that method after the fields are set to \code{null}.




\Subsection[subtyping]{Subtyping in FOIGJ}


An environment~$\Gamma$ is a finite mapping from variables~\hx and locations~\hl to types~\hT,
    e.g.,~$\hx:\hT \in \Gamma$.
The location types define the ownership tree~$\Oprec$ (or without reflexivity~$\OprecNotEqual$).
The set of currently executing constructors is denoted~$K$.
In addition,~$\Gamma$ maps the immutability parameter~\hI to its bound according
    to the current method's guard (\code{IG} in \Ref{Figure}{syntax}).
For example,~$\hI:\Raw \in \Gamma$ when typing the expression \he in method \code{build} above.
%\code{<I extends Mutable>? T foo() \lb~return e; \rb}


\Ref{Figure}{subtyping} shows FOIGJ subtyping rules.
Rules~\RULE{S1}--\RULE{S4} are the same as FGJ rules:
    \RULE{S1} means that a generic variable is a subtype of its bound,
    \RULE{S2} is reflexivity, \RULE{S3} is transitivity, and \RULE{S4} is that subclassing defines subtyping.
Rules~\RULE{S5}--\RULE{S7} show subtyping among non-variable immutability parameters
    as shown in \Ref{Figure}{owners-and-immutability-params}b.
Rule~\RULE{S8} defines covariant subtyping for the immutability parameter.
Rule~\RULE{S9} formalizes subtyping with a wildcard owner.

The last four rules \RULE{S10}--\RULE{S13}
    are concerned with \emph{cookers} such as~$\Immut_\hl$.
Recall that an object is cooked when its cooker~\hl is constructed,
    i.e., the constructor of~\hl is no longer executing:~$\hl \not \in K$.
Rule~\RULE{S10} views the type as \Raw, while rules~\RULE{S11}--\RULE{S12} shows the equivalence to \Immut.
Note that subtyping is no longer antisymmetric,
    i.e., there are non-equal types~$\hT_1$ and~$\hT_2$ for which~$\hT_1 \st \hT_2 \st \hT_1$.
For example,~$\hT_1=\code{C<O,Immut}_{\code{l}}\code{>}$ and~$\hT_2=\code{C<O,Immut>}$,
    when~$\code{l} \not \in K$.
In fact, this is not surprising because these types both represent immutable object,
    and after the cooker is cooked, the identity of the cooker is irrelevant.

\paragraph{Cooker vs.\ owner}
Rule~\RULE{S13} assumes that the cooker is inside the owner ($\hl \OprecNotEqual \code{NO}$),
    which means the object might came from the outside.
This rule addresses the difference between the cooker of (i)~a location~\hl
    or (ii)~that of an expression such as field access~\code{l.f}:
    (i) location~\hl will be cooked \emph{exactly} when the constructor of~$\Cooker{\hl}$ is finished, however,
    (ii) the cooker of~\code{l.f} is an \emph{over-approximation}, i.e.,
        the object stored in that field might have been cooked earlier.
Rule~\RULE{S13} allows an over-approximation only when the cooker is inside the owner.

Consider this example:
\begin{algorithmic}
\STATE $\code{class Foo<O,I> \lb~Date<O,I> same;}$
\STATE $\code{~<I extends Raw>? Foo(Date<O,I> d) \lb{}~same=d;~\rb~~\rb}$
\end{algorithmic}
Field~\code{same} is assigned from the outside, but it might still be \this-owned.
We will show the reduction of two expressions: one where \code{same} is assigned a cooked (outside) date,
    and one with a raw date.
The expressions are inside the constructor of some object~\code{b}
    whose cooker is~\code{b} itself.

The reduction of the first expression:
\begin{algorithmic}
\STATE \code{new Foo<This,Immut>(new Date<This,Immut>())}
\end{algorithmic}
results in the heap:
$H=\{
\code{d1} \mapsto \code{Date<b,Immut}_{\code{d1}}\code{>()} ,
\code{f1} \mapsto \code{Foo<b,Immut}_{\code{f1}}\code{>(d1)}
%K \mapsto \{ \code{f1} \}
\}$.
Note that the type of~\code{d1} must be a subtype of \code{f1.same}
    in a well-typed heap (formally defined later).
The type of~\code{d1} is a subtype of \code{Date<b,Immut>}
    (because $\code{d1} \not\in K$ in rule~\RULE{S12}),
    which is a subtype of $\code{Date<b,Immut}_{\code{f1}}\code{>}$
    (because $\code{f1} \OprecNotEqual \code{b}$ in rule~\RULE{S13}).
Phrased differently, the cooker of \code{f1.same} is \code{f1},
    but it may point to an object that was cooked before,
    and indeed it points to an object whose cooker is \code{d1}
    (so it is an over-approximation).


The reduction of the second expression:
\begin{algorithmic}
\STATE \code{new Foo<This,I>(new Date<This,I>())}
\end{algorithmic}
results in the heap (because~$\hI=\code{Immut}_{\code{b}}$):
$H=\{
\code{d2} \mapsto \code{Date<b,Immut}_{\code{b}}\code{>()} ,
\code{f2} \mapsto \code{Foo<b,Immut}_{\code{b}}\code{>(d2)}
\}$.
Note that in this case, both~\code{d2} and~\code{f2} have the same cooker~\code{b}.
The type of \code{f2.same} is $\code{Date<b,Immut}_{\code{b}}\code{>}$,
    and because $\code{b} \not \OprecNotEqual \code{b}$ (see rule~\RULE{S13}),
    then we know that this is not an over-approximation,
    i.e., that field points to an object whose cooker must be \code{b}.

To summarize, consider a type $\code{Foo<o,Immut}_{\code{c}}\code{>}$.
If the cooker~\code{c} is inside the owner~\code{o} ($\code{c} \OprecNotEqual \code{o}$),
    or the cooker is cooked ($\code{c} \not \in K$),
    then the type is an over-approximation,
    i.e., it can point to any \Immut object (that is, to any object with cooker~$\code{c'} \not\in K$).
Otherwise, it points to an object whose cooker is exactly~\code{c}.
Formally,
\begin{Lemma}[Exact-Cooker]
If $\KGdash \code{C<MO,IP>} \st \code{C'<NO,Immut}_{\hl}\code{>}$,
    $\hl \not\OprecNotEqual \code{NO}$, and $\hl \in K$,
    then~$\code{IP}=\code{Immut}_{\hl}$.
\end{Lemma}

We also prove in the technical report that:
\begin{Lemma}[Owners-Invariant]
If $\KGdash \code{C<MO,IP>}\st\code{C'<MO',IP'>}$, then
    (i)~$\code{MO'}\neq\code{?} \Rightarrow \code{MO}=\code{MO'}$,
    (ii)~$(\code{IP'}\neq\Immut_\hl \text{~or~} \hl \not\OprecNotEqual \code{MO'}) \Rightarrow \KGdash \code{IP} \st \code{IP'}$, and
    (iii)~\code{C} is a subclass of~\code{C'},
    (iv)~$\KGdash \code{D<l,IP>}\st\code{D<l,IP'>}$ for any class~\code{D} and location~\hl where~$\code{MO'} \Oprec \hl$.
\end{Lemma}

% Trying to explain why the outside world cannot see the cooking phase
%Finally, note that the subtyping rules guarantee that
%    there cannot be an immutable reference to a raw object, because \Immut is not a subtype of \Raw.
%(Note that the outside world can have a ReadOnly reference to a cooking object.)
%This follows directly from the subtyping rules, because an Immut reference
%must point to an object with immutability Immut_l where l is not in K.
%(We can add this lemma.)


\Subsection[type-checking]{Typing rules of FOIGJ}

\input{formal-typing}

%Next we proceed to define the typing rules.
\paragraph{Auxiliary functions}
We use the following auxiliary functions:
    $\fields{}(\hC)$ returns all the field names (including inherited fields) of class~\hC,
    $\ftype{}(\hf,\hC)$ returns the type of field~\hf in class~\hC,
    $\mtype{}(\hm,\hC)$ returns the type of method~\code{m} in class~\hC,
    and $\mbody{}(\hm,\hC)$ returns its body.
Their definitions are based on their counterparts in FJ, and thus omitted from this paper.
In addition, function
    $\mguard{}(\hm,\hC)$ returns the method's guard (\code{IG} in \Ref{Figure}{syntax}).

We overload the auxiliary functions above to work also for types ($\hT=\code{C<MO,IP>}$) and not just classes (\hC)
    by substituting~\code{$[$MO$/$O$,$IP$/$I$]$}.
However, we also need to carefully substitute \This when the receiver is \this or locations.
Function~$\ftype{}(\underline{\he},\hf,\hT)$ returns the type of the field access~\code{\underline{e}.f}
    where \hT is the type of~\he, or \code{error} if the access is illegal.
For example,
\beqst
\code{\ftype{}(ownedD,Foo)} & = \code{Date<This,I>} \\
\code{\ftype{}(\this,ownedD,Foo<O,Immut>)} & = \code{Date<This,Immut>}\\
\code{\ftype{}(\this.f,ownedD,Foo<O,Immut>)} & = \code{error}\\
\code{\ftype{}(l,ownedD,Foo<o,Immut}_\hc\code{>)} & = \code{Date<l,Immut}_\hc\code{>}\\
\eeq
Formally, \code{\ftype{}(e,f,C<MO,IP>)=$[$MO$/$O$,$IP$/$I$,$z$/$This$]$\ftype{}(f,\hC)},
    where (i)~$\code{z}=\hl$ if~$\he=\hl$, (ii)~$\code{z}=\This$ if~$\he=\this$, (iii)~otherwise~$\code{z}=\code{error}$
    (and if a type contains \code{error} then it means the call to $\ftype$ failed).
When we know the field is not \this-owned, then the expression~\he is not used,
    and we write~$\ftype{}(\bot,\hf,\hC)$.
However, if the field is \this-owned, then~\he must be \this or a location~\hl.

Recall that \textbf{Field access rule} in \Ref{Figure}{oigj-typing-rules}
    required that
    \this-owned fields can be accessed only via \this.
At run time, \this is substituted with a location~\hl.
Therefore, there is a \emph{duality} between \this and a location~\hl in the definition of~\ftype.
For example, the field access \code{\underline{this}.ownedD} of type \code{Date<\underline{This},I>}
    is legal because we accessed a \this-owned field via \underline{\this}.
At run time, \this is substituted with some location~\hl,
    and the access \code{\underline{l}.ownedD} of type \code{Date<\underline{l},\ldots>} is now still legal because
    we accessed a \this-owned field via \underline{a location~\hl}.
Note that if the access is not done via a location, e.g., \code{bar.l.ownedD},
    then we cannot type-check the resulting expression (because we do not know what should be the substitute for \This).

There is a similar duality
    in \textbf{Field assignment rule} part (ii),
    that checks that \Raw is transitive for \this or \this-owned objects.
The dual of \this is a location~\hl,
    and the dual of a \this-owned object (\code{C<This,I>})
    is an object whose cooker is not inside its owner ($\code{C<o,Immut}_\hl\code{>}$ where~$\hl \not \OprecNotEqual \code{o}$).
The second duality holds because, for type \code{C<This,I>}, the cooker (\hI) is never inside the owner (\This).
At run time, the owner will be the location of \this,
    and the cooker is either \this or some other object that was created before \this,
    i.e., the cooker is never inside the owner (but they might be equal).

Function~\isTransitive{} checks whether \Raw is transitive.
The underlined part shows the \emph{dual} version of \textbf{Field assignment rule} part (ii):
    (i)~\this vs.~$\hl'$,
    and (ii)~$\code{MO}=\This$ vs.~$\hl \not \OprecNotEqual \code{MO}$.

\begin{algorithmic}
\STATE $\isTransitive{}(\he,\Gamma,\code{C<MO,IP>})~=$
\STATE $~~\big(\code{IP}=\hI \text{~and~} \Gamma(\hI)=\Raw \Rightarrow (\code{e=\this{}}\text{~or~~}\code{MO}=\This)\big)\text{~or~}$
\STATE $~~\gap~~~ \big(\underline{\code{IP}=\Immut_\hl \Rightarrow (\code{e=l'}\text{~or~}\hl \not \OprecNotEqual \code{MO})}\big)$
% I don't need: \hl\in K  , because I requested that \code{IP} \st \Raw
\end{algorithmic}



\paragraph{Typing class declarations}
FOIGJ program consists of class declarations followed by the program's expression.
Next, we describe in words the rules for typing the class declarations,
    and the rules for typing an expression are given formally in \Ref{Figure}{expressions}.
When typing an expression, we assumed the class declarations are well-formed.

To check that class declarations are well-formed, FOIGJ first
    performs all the checks done in FJ,
    e.g., that there are no cycles in the inheritance relation,
    that field and method names are unique in a class,
    that \this is not a legal method parameter name,
    that an overriding method maintains the same signature, etc.
FOIGJ performs additional checks related to method guards when typing method declarations,
    i.e., we modify rule \formalrule{T-Method} in FJ as follows:
    (i)~An overriding method can only make the guard weaker,
        i.e., if a method with guard \code{IG} overrides one with guard \code{IG'}
            then~$\code{IG'} \st \code{IG}$.
    (ii)~In class~\hC, when typing a method:
        $\code{<I extends IG>?} ~ \code{FT} ~ \hm\hparen{\ol{\code{T}} ~ \ol{\hx}} ~ \lb\ \hreturn ~ \he\texttt{;} \rb$\\
        we use an environment~$\Gamma$ in which the bound of~\hI is \code{IG},
        i.e.,~$\Gamma=\{\hI:\code{IG}, \ol{\hx}:\ol{\code{T}}, \this:\code{C<O,I>}\}$,
        and we must prove that~$\emptyset,\Gamma \vdash \he:\code{S}$
        and~$\emptyset,\Gamma \vdash \code{S} \st \code{FT}$.
    Finally, we require that if~$\code{IG}=\ReadOnly$ then~$\Ifn{\hT_i}\neq\hI$.
This last requirement is not really a limitation, because
    a programmer can replace \hI with \ReadOnly for parameters in readonly methods,
    and previously legal programs would remain legal.
(This requirement is needed to prove preservation for the congruence rule of method receiver,
    see our technical report for details.)


\input{formal-reduction}

\paragraph{Typing expressions}
\Ref{Figure}{expressions} shows the typing rules for expressions in FOIGJ.
Most of these rules are a direct translation from \Ref{Figure}{oigj-typing-rules}.
The main challenge was handling \emph{wildcards} correctly without resulting in wildcard-capture.
Rule \RULE{T-Field-assignment} requires that $\code{MO} \neq \code{?}$,
    i.e., one cannot assign to an object with unknown owner.
Typing method parameters is similar to typing field-assignment,
    however, method parameters can have a wildcard owner whereas fields cannot
    (see the difference between \hT and \code{FT} in \Ref{Figure}{syntax}).
Thus, rule \RULE{T-Invoke} requires that
    $\Ofn{\ol{\code{T}}}=\code{?} \Rightarrow \Ofn{\ol{\code{U}}}=\code{?}$,
    i.e., if~$\hT_i = \hC\code{<?,IP>}$ then~$\code{U}_i = \hC\code{<?,IP'>}$.
I.e.,
%In other words,
%Phrased differently,
    if the owner of $\he_0$ is unknown, then the owner of the method parameters cannot be \hO.

Rule \RULE{T-New} performs less checks compared to a method call
    (e.g., no need to check the guard, \isTransitive, nor wildcards)
    because \code{build} has several restrictions:
    its guard is \Raw and it does not contain wildcards nor \this-owned parameters.
Because \This does not appear in the signature of \code{build},
    we know that $\mtype{}$ will not use~$\bot$ in the call:
    $\mtype{}(\bot,\code{build},\code{C<FO,VI>})$.

An expression/type is called \emph{closed} if it does not contain
    any free variables (e.g., wildcards, \this, \hI, \hO, or \This),
    but it may contain \World, \ReadOnly, \Mutable, \Immut, $\Immut_\hl$ or $\hl$.
Note that the type of a closed expression is also closed.
\begin{Lemma}[closed]
If~$\KGdash \he' : \hT'$ and $\he'$ is closed and $\he'\neq\code{null}$, then $\hT'$ is closed.
\end{Lemma}
\noindent
The delicate part of the proof is showing that~$\hT'$ does not contain \This.
Note that~$\ftype$ returns a type with \This only if~$\he=\this$
    (which cannot happen since \he is closed).





\Subsection[reduction]{Reduction rules of FOIGJ}
The initial expression to be reduced is \emph{closed},
    and we guarantee that a closed expression is always reduced to another closed expression:
%    and closed expressions have closed types.
\begin{Lemma}[reduction-closed]
If~\he is closed and~$K \vdash H,\he \reducesto H',\he'$, then~$\he'$ is closed.
\end{Lemma}

The heap (or store)~$H$ maps each location~\hl to an object~$\hC\code{<NO,NI>}\hparen{\ol{\hv}}$,
    where~$\OwnerH{\hl} = \code{NO}$ is its owner,
    and $\IfnH{\hl} = \code{NI}$ is its immutability,
    and $\ol{\hv}$ are the values of its fields.
If~$\code{NI}=\Immut_{\hl'}$ then we say that its cooker is~$\CookerH{\hl} = \hl'$.
(We added the subscript $H$ to the functions that return the owner, immutability and cooker,
    in order to explicitly show the dependence on the heap.)
We define a \emph{heap-typing}~$\Gamma_H: \hl \mapsto \hT$ that gives a type to each location
    in the obvious way (simply removing the list of fields~$\hparen{\ol{\hv}}$).

The set of currently executing constructors is~$K$.
A heap~$H$ is \emph{well-typed for~$K$} if it satisfies two conditions:
(i)~Each field location is a subtype (using~$K,\Gamma_H$) of the declared field type,
    i.e., for every location~\hl, where $H[\hl] = \code{C<NO,NI>(}\ol{\hv}\code{)}$ and~$\fields{}(\hC)=\ol{\hf}$,
        and
        for every field~$\hf_i$, we have that either $\hv_i=\code{null}$ or
        $K,\Gamma_H \vdash \Gamma_H(\hv_i) \st \ftype{}(\hl,\hf_i,\code{C<NO,NI>})$.
(ii)~There is a linear order~$\Tprec$ over~$\dom{}(H)$ such that for every location~\hl,
        $\OwnerH{\hl}=\World$ or $\OwnerH{\hl} \TprecNotEqual \hl$, and $\IfnH{\hl}=\Mutable$ or $\CookerH{\hl} \Tprec \hl$.
The linear order~$\Tprec$ can order the objects according to their \emph{creation time},
    because~$\OwnerH{\hl}$ is always created before~$\hl$,
    and~$\CookerH{\hl}$ is either~\hl or created before~$\hl$.

In our technical report we prove that if $H$ is {well-typed for~$K$} then
    (a)~owner-as-dominator holds (\Ref{Lemma}{owner-as-dominator}), and
    (b)~$H$ is well-typed for any subset of~$K$ (\Ref{Lemma}{well-typed}).
Part (b) is not trivial, because the subtyping relation for a subset of~$K$ is different because raw objects become immutable.
Intuitively, during execution objects become cooked (when their cooker is removed from~$K$), and
    therefore \Ref{Lemma}{well-typed} guarantees that the heap remains well-typed when~$K$ decreases.

\begin{Lemma}[owner-as-dominator]
If heap~$H$ is well-typed for~$K$, then for every location~$\hl \in \dom{}(H)$,
    $
    \hl \mapsto \hC\code{<NO,NI>}\hparen{\ol{\hv}}
    $,
    then either~$\hv_i=\code{null}$ or~$\hl \Oprec \OwnerH{\hv_i}$.
\end{Lemma}
\begin{Lemma}[well-typed]
Given a heap~$H$ that is well-typed for~$K$,
    then for any~$S \subset K$,
    the heap~$H$ is well-typed for~$S$.
\end{Lemma}



\Ref{Figure}{reduction} presents the reduction rules in a small-step notation,
    excluding all congruence rules except \RULE{R-c1}. % FGJ called them 'congruence rules'

Rule \RULE{R-return} ignores the return value of \code{build} and returns~\hl.
Rule \RULE{R-Field-Access} is trivial.
Rule \RULE{R-Field-assignment} enforces our immutability guarantee (only mutable or raw objects can be mutated)
    and our ownership guarantee (owner-as-dominator, i.e.,~\hl can point to~$\hv'$ iff~$\hl \Oprec \OwnerH{\hv'}$).
Rule \RULE{R-Invoke}
    finds the method body according to the receiver,
    and substitutes all the free variables in the method body.

Rule~\RULE{R-c1} is the congruence rule for \code{e;return l}.
Note that this rule is the only place the set~$K$ is modified,
    i.e., when reducing~\he, the set of ongoing constructors is~$K \cup \{\hl\}$.
It is easy to prove that if~$K \vdash H,\he \reducesto H',\he'$ then
    $\Gamma_H \subseteq \Gamma_{H'}$.
The other congruence rules are not shown because they are trivial,
    e.g., in order to reduce a method call~$\he_0\code{.m(}\ol{\he}\code{)}$,
    we first reduce~$\he_0$ to a location, then reduce the first argument to a value, etc.

Rule \RULE{R-New} creates a new location~\hl, sets the fields to \code{null},
    sets the cooker of~\hl (\code{VI'})
    and finally calls \code{build}.
In order to build the newly created object~\hl, then it must be raw, i.e., its cooker~\code{VI'} must be in~$K$.
(Note that~\hl will be in~$K$ according to \RULE{R-c1}.) % when we reduce~$H',\code{l.build(\ldots)}$ we have that~$\hl \in K$.
Therefore, if~$\code{VI}=\Immut_{\hc}$ and~$\hc \not \in K$, then we must set the cooker to~\hl.
This can happen if there is a method that returns~\code{new C<O,I>(\ldots)}
    and the receiver is a \emph{cooked} immutable object. % (so~\hI will be replaced with~$\Immut_{\hc}$ and~$\hc \not \in K$)




\Subsection[soundness]{Guarantees of FOIGJ}
We now turn to prove various properties of FOIGJ, including preservation theorem,
    ownership and immutability guarantees, and an erasure property.
In the remainder of this section, we assume that reduction does not get stuck on \emph{null-pointer exceptions},
    i.e., the receiver/target of field access, assignment and method calls is never \code{null}.
Under this assumption,
    then~\he can always be reduced to another expression~$\he'$.

Before stating the preservation theorem,
    we need to establish a connection between~$K$ and the reduced expression~\he, which may contain~\code{return l}.
Given an expression~\he, we define~$K(\he)$ to be the set
    of all ongoing constructors in~\he, i.e., all the locations in subexpressions~\code{e';return l}.
Formally,~$K(\code{e;return l}) = K(\code{e}) \cup \{ l \}$, and for any other expression we just recurse into all subexpressions,
    e.g.,~$K(\code{e.f=e'}) = K(\code{e}) \cup K(\code{e'})$.

We will maintain the invariant that~$H$ is well-typed for~$K \cup K(\he)$.
From \Ref{Lemma}{well-typed}, then~$H$ will also be well-typed for~$K$.
Initially, we start with a closed expression~\he without any locations (therefore~$K(\he)=\emptyset$),
    an empty heap~$H$, and an empty set of constructors~$K$.

\begin{Theorem}[preservation]
  \textbf{(Progress and Preservation)}
    For every closed expression~$\he \neq \hv$, $K$, and $H$,
        if $K,\Gamma_{H} \vdash \he : \hT$ and $H$ is well-typed for~$K \cup K(\he)$,
        then there exists~$H',\he',\hT'$ such that~$K \vdash H,\he \reducesto H',\he'$,
        $H'$ is well-typed for~$K \cup K(\he')$, \hT, \hT', and $\he'$ are closed,
        $K,\Gamma_{H'} \vdash \he':\hT'$, and~$K,\Gamma_{H'} \vdash \hT' \st \hT$.
\end{Theorem}
\noindent
Proved by showing there is always (exactly) one applicable reduction rule,
    which preserves subtyping.
From \Ref{Lemma}{reduction-closed}, we know that~$\he'$ is closed,
    and from \Ref{Lemma}{closed}, we know that $\hT$ and $\hT'$ are closed.
Next we mention some highlights from the proof.
In rule~\RULE{R-return}, we have that~$K(\he') = K(\he) \setminus\{\hl\}$, but even though we shrink~$K$, we still have a well-typed heap from \Ref{Lemma}{well-typed}.
In rule~\RULE{R-Field-Assignment}, \Ref{Lemma}{owner-as-dominator} shows that the assumption $\hl \Oprec \OwnerH{\hv'}$ holds,
    and the resulting heap is well-typed for~$K \cup K(\he')$ because~$K(\he')=\{\}$ and from \RULE{T-Field-Assignment}.
In rule~\RULE{R-New}, we need to type the call~$\hl\code{.build}\hparen{\ol{\hv}}$,
    and for parameters with immutability~$\hI$, we use the subtyping rule~\RULE{S13}.

Our ownership and immutability guarantees follow directly from the reduction rules,
    because rule \RULE{R-Field-assignment} enforces them.


\Ref{Theorem}{Erasure} shows that there is no need to maintain at run time~$K$
    nor to store the owner and immutability parameter of each object.
Formally, we define an erased heap structure~$E(H)$ that maps location to objects without these parameters,
    i.e.,~$\hl \mapsto \code{C(}\ol{\hv}\code{)} \in E(H)$.
We define the erasure of an expression~$\he$,~$E(\he)$, by deleting all generic parameters,
    and define new reduction rules~$\reducesto_E$ in the obvious way.
\begin{Theorem}[Erasure]
  \textbf{(Erasure)}
If~$K \vdash H,\he \reducesto H',\he'$
    then\\
    $\gap \gap \gap\gap \gap~~~~~~K \vdash E(H),E(\he) \reducesto_{E} E(H'),E(\he')$.
\end{Theorem}

% LocalWords:  wildcards FOIGJ FJ cJ oigj sameD ownedD Immut immutD FOIGJ's FGJ
% LocalWords:  FGJ's IGJ FIGJ OGJ FOGJ cJ's IG params IP readonly FO
